<html>

<head>
<title>HOL4 Metis Library Documentation</title>
</head>

<body bgcolor=white>


<h1>HOL4 Metis Library Documentation</h1>


<h2>Quick Guide to Using the HOL4 Metis Library</h2>

At the top of your proof script, write

<p>

<kbd>&nbsp load "metisLib";</kbd><br>
<kbd>&nbsp open metisLib;</kbd>

<p>

Opening the Metis library makes available the automatic provers

<p>

<kbd>&nbsp&nbsp&nbsp METIS_TAC : thm list -> tactic</kbd><br>
<kbd>&nbsp METIS_PROVE : thm list -> term -> thm</kbd>

<p>

which both take a list of theorems that are used to prove the subgoal.


<h2>Examples</h2>

<kbd>prove (``?x. x``, METIS_TAC []);</kbd>

<p>

<kbd>prove (``!x. ~(x = 0) ==> ?!y. x = SUC y``,<br>
&nbsp&nbsp&nbsp&nbsp&nbsp&nbsp METIS_TAC [numTheory.INV_SUC, arithmeticTheory.num_CASES]);</kbd>

<p>

<kbd>METIS_PROVE [prim_recTheory.LESS_SUC_REFL, arithmeticTheory.num_CASES]<br>
``(!P. (!n. (!m. m < n ==> P m) ==> P n) ==> !n. P n) ==><br>
&nbsp !P. P 0 /\ (!n. P n ==> P (SUC n)) ==> !n. P n``;</kbd>


<h2>How It Works</h2>

This is how <kbd>METIS_TAC</kbd> proves a HOL subgoal:

<p>

<ol>

<li>First some HOL conversions and tactics simplify the subgoal and
convert it to conjunctive normal form.</li>

<li>The normalized problem is mapped to first-order syntax.</li>

<li>The Metis first-order prover attacks the first-order problem,
hopefully deriving a refutation.</li>

<li>The first-order refutation is translated to a HOL proof of the
original subgoal.</li>

</ol>

<p>

For more details on the interface please refer to the <a
href="http://www.cl.cam.ac.uk/~jeh1004/research/papers/hol2fol.html">System
Description</a>. To find out more about the Metis first-order prover
(including performance information) you can visit its <a
href="http://www.cl.cam.ac.uk/~jeh1004/software/metis">own web
page</a>.


<h2>Comparison with <kbd>MESON_TAC</kbd></h2>

<kbd>METIS_TAC</kbd> is generally slower than <kbd>MESON_TAC</kbd> on
simple problems, but has better coverage. For example,
<kbd>MESON_TAC</kbd> cannot prove the following theorems:

<p>

<kbd>&nbsp METIS_PROVE [] ``?x. x``;</kbd><br>
<kbd>&nbsp METIS_PROVE [] ``p (\x. x) /\ q ==> q /\ p (\y. y)``;</kbd>

<p>

The combination of model elimination and resolution calculi in
<kbd>METIS_TAC</kbd> allows some hard theorems to be proved that are
too deep for the HOL version of <kbd>MESON_TAC</kbd>, such as the
<kbd>GILMORE_9</kbd> and <kbd>STEAM_ROLLER</kbd> problems. Also, the
ordered paramodulation used by the resolution component of
<kbd>METIS_TAC</kbd> allows it to prove harder equality problems. An
example to illustrate this is the following theorem:

<p>

<kbd>&nbsp METIS_PROVE []<br>
&nbsp ``(!x y. x * y = y * x) /\ (!x y z. x * y * z = x * (y * z)) ==><br>
&nbsp&nbsp  a * b * c * d * e * f = f * e * d * c * b * a``;</kbd>


<h2>Known Bugs</h2>

At the present time all the bugs are unknown.


<h2>Credits</h2>

The HOL4 Metis library was written by Joe Hurd, based on John
Harrison's implementation of <kbd>MESON_TAC</kbd>. The library has
been much improved by feedback from HOL4 users, especially Michael
Norrish, Konrad Slind and Mike Gordon.</li>


<h2>Change Log</h2>

<ul>

<li>Implemented a HOL specific finite model, which knows about
numbers, lists and sets.</li>

<li>Removed multiple provers, <kbd>METIS_TAC</kbd> is now solely based
on ordered resolution.</li>

<li>Changed the normalization to eliminate <kbd>let</kbd> terms.</li>

</ul>

<p>

<h3>Version 1.5: 14 January 2004</h3>

<kbd>Subgoals proved by MESON_TAC when HOL is built .......... 2010</kbd><br>
<kbd>Proved by METIS_TAC within 10s .......................... 1998</kbd><br>

<h3>Between Versions 1.4 and 1.5</h3>

<ul>

<li>Scheduling provers is no longer based on time used, but rather
number of inferences.</li>

<li>Simplification of resolution clauses using disequation literals.</li>

<li>Implemented finite models to guide clause selection in resolution.</li>

<li>The model elimination prover optimizes the order of rules and
literals within rules.</li>

</ul>

<p>

<h3>Version 1.4: 2 October 2003</h3>

<kbd>Subgoals proved by MESON_TAC when HOL is built .......... 1982</kbd><br>
<kbd>Proved by METIS_TAC within 10s .......................... 1977</kbd><br>

<h3>Between Versions 1.3 and 1.4</h3>

<ul>

<li>Added an ordered resolution prover to the default set.</li>

<li>Improved resolution performance with a special-purpose datatype
for inter-reducing equations.</li>

</ul>

<p>

<h3>Version 1.3: 18 June 2003</h3>

<kbd>Subgoals proved by MESON_TAC when HOL is built .......... 1976</kbd><br>
<kbd>Proved by METIS_TAC within 10s .......................... 1971</kbd><br>

<h3>Between Versions 1.2 and 1.3</h3>

<ul>

<li>Implemention of definitional CNF to reduce blow-up in number of
clauses (usually caused by nested boolean equivalences).</li>

<li>Resolution is more robust and efficient, and includes an option
(off by default) for clauses to inherit ordering constraints.</li>

</ul>

<p>

<h3>Version 1.2: 19 November 2002</h3>

<kbd>Subgoals proved by MESON_TAC when HOL is built .......... 1779</kbd><br>
<kbd>Proved by METIS_TAC within 10s .......................... 1774</kbd><br>

<h3>Between Versions 1.1 and 1.2</h3>

<ul>

<li>Ground-up rewrite of the resolution calculus, which now performs
ordered resolution and ordered paramodulation.</li>

<li>A single entry-point <kbd>METIS_TAC</kbd>, which uses heuristics
to decide whether to apply <kbd>FO_METIS_TAC</kbd> or
<kbd>HO_METIS_TAC</kbd>.</li>

<li><kbd>{HO|FO}_METIS_TAC</kbd> both initially operate in typeless
mode, and automatically try again with types if an error occurs during
proof translation.</li>

<li>Extensionality theorem now included in <kbd>HO_METIS_TAC</kbd> by
default.</li>

</ul>

<p>

<h3>Version 1.1: 21 September 2002</h3>

<kbd>Subgoals proved by MESON_TAC when HOL is built .......... 1745</kbd><br>
<kbd>Proved by FO_METIS_TAC within 10s ....................... 1485</kbd><br>
<kbd>Proved by HO_METIS_TAC within 10s ....................... 1698</kbd><br>
<kbd>Proved by one of {FO|HO}_METIS_TAC within 10s ........... 1717</kbd>

<h3>Between Versions 1.0 and 1.1</h3>

<ul>

<li>Added a <kbd>"metis"</kbd> entry to the HOL trace system: it nows
prints status information during proof (if HOL is in interactive
mode).</li>

<li>Restricted (universal and existential) quantifiers are now
normalized by the NNF conversion.</li>

<li>Improved performance in the model elimination proof procedure with
better caching (following a suggestion from John Harrison).</li>

<li>First-order substitutions are now fully Boultonized.</li>

<li>The first-order logical kernel automatically performs peep-hole
optimizations to keep proofs as small as possible.</li>

</ul>

<p>

<h3>Version 1.0: 18 July 2002</h3>

<kbd>Subgoals proved by MESON_TAC when HOL is built .......... 1435</kbd><br>
<kbd>Proved by FO_METIS_TAC within 10s ....................... 1240</kbd><br>
<kbd>Proved by HO_METIS_TAC within 10s ....................... 1346</kbd><br>
<kbd>Proved by one of {FO|HO}_METIS_TAC within 10s ........... 1389</kbd>

<p>

<img src="metis.jpg" alt="Metis the moon of Jupiter">

</body>

</html>
